| 1: | dbl(0) | → 0 | |
| 2: | dbl(s(X)) | → s(s(dbl(X))) | |
| 3: | dbls(nil) | → nil | |
| 4: | dbls(cons(X,Y)) | → cons(dbl(X),dbls(Y)) | |
| 5: | sel(0,cons(X,Y)) | → X | |
| 6: | sel(s(X),cons(Y,Z)) | → sel(X,Z) | |
| 7: | indx(nil,X) | → nil | |
| 8: | indx(cons(X,Y),Z) | → cons(sel(X,Z),indx(Y,Z)) | |
| 9: | from(X) | → cons(X,from(s(X))) | |
| 10: | dbl1(0) | → 01 | |
| 11: | dbl1(s(X)) | → s1(s1(dbl1(X))) | |
| 12: | sel1(0,cons(X,Y)) | → X | |
| 13: | sel1(s(X),cons(Y,Z)) | → sel1(X,Z) | |
| 14: | quote(0) | → 01 | |
| 15: | quote(s(X)) | → s1(quote(X)) | |
| 16: | quote(dbl(X)) | → dbl1(X) | |
| 17: | quote(sel(X,Y)) | → sel1(X,Y) | |
| 18: | DBL(s(X)) | → DBL(X) | |
| 19: | DBLS(cons(X,Y)) | → DBL(X) | |
| 20: | DBLS(cons(X,Y)) | → DBLS(Y) | |
| 21: | SEL(s(X),cons(Y,Z)) | → SEL(X,Z) | |
| 22: | INDX(cons(X,Y),Z) | → SEL(X,Z) | |
| 23: | INDX(cons(X,Y),Z) | → INDX(Y,Z) | |
| 24: | FROM(X) | → FROM(s(X)) | |
| 25: | DBL1(s(X)) | → DBL1(X) | |
| 26: | SEL1(s(X),cons(Y,Z)) | → SEL1(X,Z) | |
| 27: | QUOTE(s(X)) | → QUOTE(X) | |
| 28: | QUOTE(dbl(X)) | → DBL1(X) | |
| 29: | QUOTE(sel(X,Y)) | → SEL1(X,Y) | |